Unobjectionable rewrite rules for saturated arithmetic #1777

JasonGross · 2023-12-08T03:30:21Z

We don't yet include the ones that are higher-order-than 3, those need more debugging.

JasonGross · 2023-12-08T03:31:58Z

src/Rewriter/Rules.v

+            ; (forall s y x k,
+                  Z.add_get_carry_full s x (-y * k)
+                  = dlet vb := Z.sub_get_borrow_full s x (y * k) in (fst vb, - snd vb))
+            ; (forall s y x k,
+                  Z.add_get_carry_full s (-y * k) x
+                  = dlet vb := Z.sub_get_borrow_full s x (y * k) in (fst vb, - snd vb))


@jadephilipoom perhaps we should standardize on Z.add_get_carry_full and get rid of other variants?

Originally posted by @andres-erbsen in #1609 (comment)

JasonGross · 2023-12-08T03:32:57Z

src/Rewriter/Rules.v

+         ; mymap
+             do_again
+             [ (forall x y, cstZ r[0~>1] x * y = Z.zselect (cstZ r[0~>1] x) (cstZ r[0~>0] (' 0)) y)
+             ; (forall x y, y * cstZ r[0~>1] x = Z.zselect (cstZ r[0~>1] x) (cstZ r[0~>0] (' 0)) y)
+             ; (forall c M rv r0 rM, 0 ∈ r0 -> M ∈ rM -> M ∈ rv -> 2^Z.log2 (M+1) = M + 1 -> 1 <= M ->
+                  cstZ rv (Z.zselect (cstZ r[0~>1] c) (cstZ r0 ('0)) (cstZ rM ('M)))
+                  = (dlet vc := cstZZ rv r[0~>1] (Z.sub_with_get_borrow_full ('(M+1)) (cstZ r[0~>1] c) 0 0) in
+                     cstZ rv (fst vc)))
+              ; (forall rv c x y, cstZ rv (Z.zselect c x y) = dlet v := cstZ rv (Z.zselect c x y) in cstZ rv v)
+                  ]


@andres-erbsen turn mul_split with negated intput into negated mul_split first

Originally posted by @andres-erbsen in #1609 (comment)

@andres-erbsen Is this something that should be done before merging?

JasonGross · 2023-12-08T05:14:43Z

@andres-erbsen These rewrite rules break current synthesis:

Which with some casts elided is:
(λ x1,
  let x2 := Z.sub_with_get_borrow((2^51), (0, ((uint64_t)(x1[0]), 0x7ffffffffffed))) (* : uint64_t, uint1_t *) in
  let x3 := Z.sub_with_get_borrow((2^51), ((uint1_t)x2₂, ((uint64_t)(x1[1]), (2^51-1)))) (* : uint64_t, uint1_t *) in
  let x4 := Z.sub_with_get_borrow((2^51), ((uint1_t)x3₂, ((uint64_t)(x1[2]), (2^51-1)))) (* : uint64_t, uint1_t *) in
  let x5 := Z.sub_with_get_borrow((2^51), ((uint1_t)x4₂, ((uint64_t)(x1[3]), (2^51-1)))) (* : uint64_t, uint1_t *) in
  let x6 := Z.sub_with_get_borrow((2^51), ((uint1_t)x5₂, ((uint64_t)(x1[4]), (2^51-1)))) (* : uint64_t, uint1_t *) in
  let x7 := -x6₂ mod 2^64 (* : uint64_t *) in
  let x8 := Z.add_get_carry((2^51), ((uint64_t)x2₁, (uint64_t)(x7 & 0x7ffffffffffed))) (* : uint64_t, uint1_t *) in
  let x9 := Z.add_with_get_carry((2^51), ((uint1_t)x8₂, ((uint64_t)x3₁, (uint64_t)(x7 & (2^51-1))))) (* : uint64_t, uint1_t *) in
  let x10 := Z.add_with_get_carry((2^51), ((uint1_t)x9₂, ((uint64_t)x4₁, (uint64_t)(x7 & (2^51-1))))) (* : uint64_t, uint1_t *) in
  let x11 := Z.add_with_get_carry((2^51), ((uint1_t)x10₂, ((uint64_t)x5₁, (uint64_t)(x7 & (2^51-1))))) (* : uint64_t, uint1_t *) in
  let x12 := Z.add_with_get_carry((2^51), ((uint1_t)x11₂, ((uint64_t)x6₁, (uint64_t)(x7 & (2^51-1))))) (* : uint64_t, uint1_t *) in
  let x13 := x12₁ << 4 (* : uint64_t *) in
  let x14 := x11₁ * 2 (* : uint64_t *) in
  let x15 := x10₁ << 6 (* : uint64_t *) in
  let x16 := x9₁ << 3 (* : uint64_t *) in
  let x17 := x8₁ & 255 (* : uint8_t *) in
  let x18 := x8₁ >> 8 (* : uint64_t *) in
  let x19 := x18 & 255 (* : uint8_t *) in
  let x20 := x18 >> 8 (* : uint64_t *) in
  let x21 := x20 & 255 (* : uint8_t *) in
  let x22 := x20 >> 8 (* : uint64_t *) in
  let x23 := x22 & 255 (* : uint8_t *) in
  let x24 := x22 >> 8 (* : uint64_t *) in
  let x25 := x24 & 255 (* : uint8_t *) in
  let x26 := x24 >> 8 (* : uint64_t *) in
  let x27 := x26 & 255 (* : uint8_t *) in
  let x28 := x26 >> 8 (* : uint8_t *) in
  let x29 := x16 + x28 (* : uint64_t *) in
  let x30 := x29 & 255 (* : uint8_t *) in
  let x31 := x29 >> 8 (* : uint64_t *) in
  let x32 := x31 & 255 (* : uint8_t *) in
  let x33 := x31 >> 8 (* : uint64_t *) in
  let x34 := x33 & 255 (* : uint8_t *) in
  let x35 := x33 >> 8 (* : uint64_t *) in
  let x36 := x35 & 255 (* : uint8_t *) in
  let x37 := x35 >> 8 (* : uint64_t *) in
  let x38 := x37 & 255 (* : uint8_t *) in
  let x39 := x37 >> 8 (* : uint64_t *) in
  let x40 := x39 & 255 (* : uint8_t *) in
  let x41 := x39 >> 8 (* : uint8_t *) in
  let x42 := x15 + x41 (* : uint64_t *) in
  let x43 := x42 & 255 (* : uint8_t *) in
  let x44 := x42 >> 8 (* : uint64_t *) in
  let x45 := x44 & 255 (* : uint8_t *) in
  let x46 := x44 >> 8 (* : uint64_t *) in
  let x47 := x46 & 255 (* : uint8_t *) in
  let x48 := x46 >> 8 (* : uint64_t *) in
  let x49 := x48 & 255 (* : uint8_t *) in
  let x50 := x48 >> 8 (* : uint64_t *) in
  let x51 := x50 & 255 (* : uint8_t *) in
  let x52 := x50 >> 8 (* : uint64_t *) in
  let x53 := x52 & 255 (* : uint8_t *) in
  let x54 := x52 >> 8 (* : uint64_t *) in
  let x55 := x54 & 255 (* : uint8_t *) in
  let x56 := x54 >> 8 (* : uint1_t *) in
  let x57 := x14 + x56 (* : uint64_t *) in
  let x58 := x57 & 255 (* : uint8_t *) in
  let x59 := x57 >> 8 (* : uint64_t *) in
  let x60 := x59 & 255 (* : uint8_t *) in
  let x61 := x59 >> 8 (* : uint64_t *) in
  let x62 := x61 & 255 (* : uint8_t *) in
  let x63 := x61 >> 8 (* : uint64_t *) in
  let x64 := x63 & 255 (* : uint8_t *) in
  let x65 := x63 >> 8 (* : uint64_t *) in
  let x66 := x65 & 255 (* : uint8_t *) in
  let x67 := x65 >> 8 (* : uint64_t *) in
  let x68 := x67 & 255 (* : uint8_t *) in
  let x69 := x67 >> 8 (* : uint8_t *) in
  let x70 := x13 + x69 (* : uint64_t *) in
  let x71 := x70 & 255 (* : uint8_t *) in
  let x72 := x70 >> 8 (* : uint64_t *) in
  let x73 := x72 & 255 (* : uint8_t *) in
  let x74 := x72 >> 8 (* : uint64_t *) in
  let x75 := x74 & 255 (* : uint8_t *) in
  let x76 := x74 >> 8 (* : uint64_t *) in
  let x77 := x76 & 255 (* : uint8_t *) in
  let x78 := x76 >> 8 (* : uint64_t *) in
  let x79 := x78 & 255 (* : uint8_t *) in
  let x80 := x78 >> 8 (* : uint64_t *) in
  let x81 := x80 & 255 (* : uint8_t *) in
  let x82 := x80 >> 8 (* : uint8_t *) in
  x17 :: x19 :: x21 :: x23 :: x25 :: x27 :: x30 :: x32 :: x34 :: x36 :: x38 :: x40 :: x43 :: x45 :: x47 :: x49 :: x51 :: x53 :: x55 :: x58 :: x60 :: x62 :: x64 :: x66 :: x68 :: x71 :: x73 :: x75 :: x77 :: x79 :: x81 :: x82 :: []
)
Error in converting ToBytes to Go:
Invalid identifier in arithmetic expression (mod)

Can you take over debugging here?

For mit-plv#1609 and mit-plv#1777

For #1609 and #1777

For https://github.com/mit-plv/fiat-crypto/pull/1609 We don't yet include the ones that are higher-order-than 3, those need more debugging. Co-authored-by: Andres Erbsen <[email protected]> <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ 119m55.01s | 2852288 ko | Total Time / Peak Mem | 116m54.82s | 2852504 ko || +3m00.19s || -216 ko | +2.56% | -0.00% ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ 4m23.28s | 1922200 ko | Rewriter/Passes/ArithWithCasts.vo | 3m44.64s | 1804812 ko || +0m38.63s || 117388 ko | +17.20% | +6.50% 1m56.74s | 1630248 ko | fiat-java/src/FiatP384Scalar.java | 1m37.68s | 1868416 ko || +0m19.06s || -238168 ko | +19.51% | -12.74% 1m58.86s | 1834476 ko | fiat-bedrock2/src/p384_32.c | 1m40.20s | 1821748 ko || +0m18.65s || 12728 ko | +18.62% | +0.69% 1m57.91s | 1645388 ko | fiat-json/src/p384_scalar_32.json | 1m39.64s | 2106288 ko || +0m18.26s || -460900 ko | +18.33% | -21.88% 0m55.68s | 1150564 ko | Rewriter/Passes/Arith.vo | 0m40.86s | 1092012 ko || +0m14.82s || 58552 ko | +36.27% | +5.36% 2m00.58s | 2234976 ko | fiat-bedrock2/src/p384_scalar_32.c | 1m47.08s | 2226524 ko || +0m13.50s || 8452 ko | +12.60% | +0.37% 1m56.68s | 1764652 ko | fiat-java/src/FiatP384.java | 1m44.50s | 1969328 ko || +0m12.18s || -204676 ko | +11.65% | -10.39% 1m54.76s | 1908628 ko | fiat-json/src/p384_32.json | 1m43.69s | 2004176 ko || +0m11.06s || -95548 ko | +10.67% | -4.76% 1m57.28s | 1615084 ko | fiat-zig/src/p384_scalar_32.zig | 1m46.91s | 1733780 ko || +0m10.37s || -118696 ko | +9.69% | -6.84% 1m54.55s | 2074740 ko | fiat-zig/src/p384_32.zig | 1m44.61s | 1626180 ko || +0m09.93s || 448560 ko | +9.50% | +27.58% 1m55.94s | 2145952 ko | fiat-go/32/p384scalar/p384scalar.go | 1m48.27s | 1630928 ko || +0m07.66s || 515024 ko | +7.08% | +31.57% 1m57.76s | 1764936 ko | fiat-rust/src/p384_scalar_32.rs | 1m51.87s | 1768464 ko || +0m05.88s || -3528 ko | +5.26% | -0.19% 1m54.58s | 1597680 ko | fiat-rust/src/p384_32.rs | 1m48.64s | 1718060 ko || +0m05.93s || -120380 ko | +5.46% | -7.00% 1m54.56s | 1708700 ko | fiat-c/src/p384_scalar_32.c | 1m49.11s | 1518820 ko || +0m05.45s || 189880 ko | +4.99% | +12.50% 1m51.99s | 1734444 ko | fiat-c/src/p384_32.c | 1m46.30s | 1630176 ko || +0m05.69s || 104268 ko | +5.35% | +6.39% 1m45.33s | 1889064 ko | Bedrock/End2End/X25519/AddPrecomputed.vo | 1m49.74s | 1889060 ko || -0m04.41s || 4 ko | -4.01% | +0.00% 5m27.35s | 2852288 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo | 5m31.22s | 2852504 ko || -0m03.87s || -216 ko | -1.16% | -0.00% 2m33.52s | 1607452 ko | Rewriter/Passes/NBE.vo | 2m37.17s | 1607512 ko || -0m03.65s || -60 ko | -2.32% | -0.00% 0m37.77s | 110828 ko | fiat-json/src/p521_32.json | 0m33.99s | 114180 ko || +0m03.78s || -3352 ko | +11.12% | -2.93% 0m37.53s | 62756 ko | fiat-java/src/FiatP521.java | 0m33.77s | 62456 ko || +0m03.75s || 300 ko | +11.13% | +0.48% 1m50.62s | 1393276 ko | Rewriter/Passes/ToFancyWithCasts.vo | 1m53.15s | 1392880 ko || -0m02.53s || 396 ko | -2.23% | +0.02% 0m42.34s | 1859688 ko | ExtractionOCaml/bedrock2_saturated_solinas | 0m40.29s | 1851720 ko || +0m02.05s || 7968 ko | +5.08% | +0.43% 0m39.48s | 1769316 ko | ExtractionOCaml/base_conversion | 0m41.92s | 1624120 ko || -0m02.44s || 145196 ko | -5.82% | +8.93% 1m49.94s | 2247636 ko | Fancy/Barrett256.vo | 1m51.28s | 2284788 ko || -0m01.34s || -37152 ko | -1.20% | -1.62% 1m47.35s | 1832408 ko | fiat-go/32/p384/p384.go | 1m49.23s | 1724040 ko || -0m01.87s || 108368 ko | -1.72% | +6.28% 1m32.25s | 2164300 ko | SlowPrimeSynthesisExamples.vo | 1m33.38s | 2139896 ko || -0m01.12s || 24404 ko | -1.21% | +1.14% 0m51.90s | 1016836 ko | Rewriter/Passes/MultiRetSplit.vo | 0m53.14s | 1016808 ko || -0m01.24s || 28 ko | -2.33% | +0.00% 0m47.25s | 2146984 ko | ExtractionOCaml/solinas_reduction | 0m45.91s | 2147072 ko || +0m01.34s || -88 ko | +2.91% | -0.00% 0m45.18s | 2146856 ko | ExtractionOCaml/word_by_word_montgomery | 0m46.83s | 2147056 ko || -0m01.64s || -200 ko | -3.52% | -0.00% 0m43.40s | 1864240 ko | ExtractionOCaml/bedrock2_dettman_multiplication | 0m41.96s | 1870364 ko || +0m01.43s || -6124 ko | +3.43% | -0.32% 0m41.82s | 1863680 ko | ExtractionOCaml/unsaturated_solinas | 0m43.45s | 1863368 ko || -0m01.63s || 312 ko | -3.75% | +0.01% 0m29.25s | 1544592 ko | StandaloneDebuggingExamples.vo | 0m30.51s | 1556744 ko || -0m01.26s || -12152 ko | -4.12% | -0.78% 0m16.94s | 283032 ko | fiat-go/64/p434/p434.go | 0m18.07s | 247128 ko || -0m01.12s || 35904 ko | -6.25% | +14.52% 0m16.74s | 2204356 ko | ExtractionHaskell/with_bedrock2_solinas_reduction.hs | 0m17.83s | 2237008 ko || -0m01.08s || -32652 ko | -6.11% | -1.45% 0m16.25s | 253040 ko | fiat-rust/src/p434_64.rs | 0m17.99s | 278560 ko || -0m01.73s || -25520 ko | -9.67% | -9.16% 8m28.15s | 2591812 ko | Bedrock/End2End/X25519/GarageDoor.vo | 8m27.82s | 2587848 ko || +0m00.32s || 3964 ko | +0.06% | +0.15% 1m51.16s | 1612836 ko | Bedrock/End2End/X25519/Field25519.vo | 1m52.02s | 1604084 ko || -0m00.86s || 8752 ko | -0.76% | +0.54% 0m56.72s | 707388 ko | Rewriter/RulesProofs.vo | 0m55.84s | 703908 ko || +0m00.87s || 3480 ko | +1.57% | +0.49% 0m49.15s | 2147776 ko | ExtractionOCaml/bedrock2_solinas_reduction | 0m48.43s | 2147920 ko || +0m00.71s || -144 ko | +1.48% | -0.00% 0m48.64s | 1869620 ko | Fancy/Montgomery256.vo | 0m48.94s | 1855572 ko || -0m00.29s || 14048 ko | -0.61% | +0.75% 0m48.41s | 2147988 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery | 0m48.03s | 2147920 ko || +0m00.37s || 68 ko | +0.79% | +0.00% 0m48.12s | 2148012 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery | 0m47.94s | 2147964 ko || +0m00.17s || 48 ko | +0.37% | +0.00% 0m47.07s | 2148072 ko | ExtractionOCaml/bedrock2_unsaturated_solinas | 0m46.98s | 2147976 ko || +0m00.09s || 96 ko | +0.19% | +0.00% 0m46.31s | 2148036 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas | 0m46.12s | 2147932 ko || +0m00.19s || 104 ko | +0.41% | +0.00% 0m42.55s | 1864184 ko | ExtractionOCaml/bedrock2_base_conversion | 0m41.57s | 1864708 ko || +0m00.97s || -524 ko | +2.35% | -0.02% 0m42.07s | 1864464 ko | ExtractionOCaml/with_bedrock2_base_conversion | 0m41.20s | 1823744 ko || +0m00.86s || 40720 ko | +2.11% | +2.23% 0m41.68s | 1858816 ko | ExtractionOCaml/with_bedrock2_saturated_solinas | 0m40.96s | 1851212 ko || +0m00.71s || 7604 ko | +1.75% | +0.41% 0m41.66s | 1859960 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication | 0m41.21s | 1851288 ko || +0m00.44s || 8672 ko | +1.09% | +0.46% 0m41.50s | 1857940 ko | ExtractionOCaml/with_bedrock2_solinas_reduction | 0m41.06s | 1849540 ko || +0m00.43s || 8400 ko | +1.07% | +0.45% 0m40.74s | 62064 ko | fiat-go/32/p521/p521.go | 0m41.26s | 68256 ko || -0m00.51s || -6192 ko | -1.26% | -9.07% 0m40.14s | 1864708 ko | ExtractionOCaml/dettman_multiplication | 0m40.52s | 1786504 ko || -0m00.38s || 78204 ko | -0.93% | +4.37% 0m38.85s | 149624 ko | fiat-bedrock2/src/p521_32.c | 0m38.98s | 143940 ko || -0m00.12s || 5684 ko | -0.33% | +3.94% 0m38.54s | 1775188 ko | ExtractionOCaml/saturated_solinas | 0m38.71s | 1764700 ko || -0m00.17s || 10488 ko | -0.43% | +0.59% 0m37.51s | 62500 ko | fiat-zig/src/p521_32.zig | 0m37.39s | 59332 ko || +0m00.11s || 3168 ko | +0.32% | +5.33% 0m37.48s | 1294192 ko | Bedrock/End2End/X25519/GarageDoorTop.vo | 0m37.27s | 1292880 ko || +0m00.20s || 1312 ko | +0.56% | +0.10% 0m37.44s | 66780 ko | fiat-c/src/p521_32.c | 0m37.77s | 60280 ko || -0m00.33s || 6500 ko | -0.87% | +10.78% 0m37.42s | 60608 ko | fiat-rust/src/p521_32.rs | 0m37.83s | 61900 ko || -0m00.40s || -1292 ko | -1.08% | -2.08% 0m37.11s | 2378444 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml | 0m37.46s | 2364772 ko || -0m00.35s || 13672 ko | -0.93% | +0.57% 0m36.36s | 2319684 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml | 0m36.69s | 2362052 ko || -0m00.32s || -42368 ko | -0.89% | -1.79% 0m36.34s | 2322608 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml | 0m36.87s | 2363400 ko || -0m00.52s || -40792 ko | -1.43% | -1.72% 0m35.65s | 2239920 ko | ExtractionOCaml/solinas_reduction.ml | 0m35.60s | 2244256 ko || +0m00.04s || -4336 ko | +0.14% | -0.19% 0m34.94s | 1413516 ko | ExtractionOCaml/perf_word_by_word_montgomery | 0m34.37s | 1401160 ko || +0m00.57s || 12356 ko | +1.65% | +0.88% 0m34.88s | 1413452 ko | ExtractionOCaml/perf_unsaturated_solinas | 0m34.36s | 1398860 ko || +0m00.52s || 14592 ko | +1.51% | +1.04% 0m34.62s | 1284740 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo | 0m35.00s | 1284680 ko || -0m00.38s || 60 ko | -1.08% | +0.00% 0m34.36s | 2237140 ko | ExtractionOCaml/word_by_word_montgomery.ml | 0m34.45s | 2220616 ko || -0m00.09s || 16524 ko | -0.26% | +0.74% 0m34.01s | 915808 ko | Rewriter/Passes/MulSplit.vo | 0m34.72s | 913152 ko || -0m00.71s || 2656 ko | -2.04% | +0.29% 0m33.79s | 2251096 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml | 0m33.50s | 2229256 ko || +0m00.28s || 21840 ko | +0.86% | +0.97% 0m33.14s | 2251808 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml | 0m33.28s | 2229952 ko || -0m00.14s || 21856 ko | -0.42% | +0.98% 0m31.42s | 2149728 ko | ExtractionOCaml/unsaturated_solinas.ml | 0m31.33s | 2124628 ko || +0m00.09s || 25100 ko | +0.28% | +1.18% 0m29.99s | 2166628 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml | 0m30.23s | 2179988 ko || -0m00.24s || -13360 ko | -0.79% | -0.61% 0m29.53s | 2156584 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml | 0m29.10s | 2125132 ko || +0m00.42s || 31452 ko | +1.47% | +1.48% 0m29.25s | 2161092 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml | 0m28.31s | 2121844 ko || +0m00.94s || 39248 ko | +3.32% | +1.84% 0m29.19s | 2161336 ko | ExtractionOCaml/bedrock2_base_conversion.ml | 0m29.47s | 2121804 ko || -0m00.27s || 39532 ko | -0.95% | +1.86% 0m29.12s | 2156880 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml | 0m29.25s | 2124968 ko || -0m00.12s || 31912 ko | -0.44% | +1.50% 0m29.07s | 2156996 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml | 0m28.94s | 2124832 ko || +0m00.12s || 32164 ko | +0.44% | +1.51% 0m28.90s | 2158288 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.ml | 0m29.11s | 2130440 ko || -0m00.21s || 27848 ko | -0.72% | +1.30% 0m27.93s | 2064324 ko | ExtractionOCaml/dettman_multiplication.ml | 0m28.14s | 2081544 ko || -0m00.21s || -17220 ko | -0.74% | -0.82% 0m27.37s | 2077984 ko | ExtractionOCaml/saturated_solinas.ml | 0m27.45s | 2061340 ko || -0m00.07s || 16644 ko | -0.29% | +0.80% 0m26.92s | 2069712 ko | ExtractionOCaml/base_conversion.ml | 0m27.35s | 2051836 ko || -0m00.42s || 17876 ko | -1.57% | +0.87% 0m25.19s | 1381372 ko | PerfTesting/PerfTestSearch.vo | 0m25.63s | 1377272 ko || -0m00.43s || 4100 ko | -1.71% | +0.29% 0m23.10s | 1189876 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m23.84s | 1191348 ko || -0m00.73s || -1472 ko | -3.10% | -0.12% 0m21.56s | 1967716 ko | ExtractionOCaml/perf_unsaturated_solinas.ml | 0m21.50s | 1905172 ko || +0m00.05s || 62544 ko | +0.27% | +3.28% 0m21.46s | 1954296 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml | 0m21.53s | 2007400 ko || -0m00.07s || -53104 ko | -0.32% | -2.64% 0m21.42s | 1364020 ko | Bedrock/End2End/RupicolaCrypto/Low.vo | 0m21.81s | 1360444 ko || -0m00.38s || 3576 ko | -1.78% | +0.26% 0m20.10s | 1163460 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m20.64s | 1164604 ko || -0m00.53s || -1144 ko | -2.61% | -0.09% 0m18.30s | 301772 ko | fiat-bedrock2/src/p434_64.c | 0m18.00s | 301336 ko || +0m00.30s || 436 ko | +1.66% | +0.14% 0m18.28s | 1142612 ko | Bedrock/Field/Translation/Proofs/Func.vo | 0m18.75s | 1141560 ko || -0m00.46s || 1052 ko | -2.50% | +0.09% 0m17.74s | 405312 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_32.c | 0m17.23s | 404568 ko || +0m00.50s || 744 ko | +2.95% | +0.18% 0m17.68s | 267560 ko | fiat-json/src/p434_64.json | 0m17.55s | 336912 ko || +0m00.12s || -69352 ko | +0.74% | -20.58% 0m17.57s | 432032 ko | fiat-bedrock2/src/p256_scalar_32.c | 0m17.05s | 461272 ko || +0m00.51s || -29240 ko | +3.04% | -6.33% 0m17.48s | 2202308 ko | ExtractionHaskell/bedrock2_solinas_reduction.hs | 0m17.75s | 2235132 ko || -0m00.26s || -32824 ko | -1.52% | -1.46% 0m17.46s | 1380556 ko | PerfTesting/PerfTestSearchPattern.vo | 0m17.92s | 1380832 ko || -0m00.46s || -276 ko | -2.56% | -0.01% 0m17.41s | 230072 ko | fiat-zig/src/p434_64.zig | 0m17.32s | 253724 ko || +0m00.08s || -23652 ko | +0.51% | -9.32% 0m17.35s | 1223956 ko | Bedrock/Field/Synthesis/New/Signature.vo | 0m17.66s | 1220516 ko || -0m00.30s || 3440 ko | -1.75% | +0.28% 0m17.35s | 2166060 ko | ExtractionHaskell/bedrock2_word_by_word_montgomery.hs | 0m17.53s | 2194808 ko || -0m00.17s || -28748 ko | -1.02% | -1.30% 0m17.28s | 2164448 ko | ExtractionHaskell/with_bedrock2_word_by_word_montgomery.hs | 0m17.52s | 2193664 ko || -0m00.23s || -29216 ko | -1.36% | -1.33% 0m17.16s | 254416 ko | fiat-c/src/p434_64.c | 0m17.42s | 251820 ko || -0m00.26s || 2596 ko | -1.49% | +1.03% 0m17.15s | 390476 ko | fiat-bedrock2/src/secp256k1_montgomery_32.c | 0m16.69s | 415512 ko || +0m00.45s || -25036 ko | +2.75% | -6.02% 0m17.01s | 351572 ko | fiat-java/src/FiatSecp256K1MontgomeryScalar.java | 0m16.40s | 455088 ko || +0m00.61s || -103516 ko | +3.71% | -22.74% 0m16.90s | 445272 ko | fiat-go/32/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go | 0m17.19s | 360700 ko || -0m00.29s || 84572 ko | -1.68% | +23.44% 0m16.86s | 1160300 ko | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m17.42s | 1157936 ko || -0m00.56s || 2364 ko | -3.21% | +0.20% 0m16.84s | 456724 ko | fiat-bedrock2/src/curve25519_scalar_32.c | 0m16.68s | 405344 ko || +0m00.16s || 51380 ko | +0.95% | +12.67% 0m16.83s | 454284 ko | fiat-json/src/secp256k1_montgomery_scalar_32.json | 0m16.39s | 468528 ko || +0m00.43s || -14244 ko | +2.68% | -3.04% 0m16.79s | 2032540 ko | ExtractionHaskell/word_by_word_montgomery.hs | 0m16.91s | 2067180 ko || -0m00.12s || -34640 ko | -0.70% | -1.67% 0m16.77s | 2093008 ko | ExtractionHaskell/solinas_reduction.hs | 0m16.77s | 2051684 ko || +0m00.00s || 41324 ko | +0.00% | +2.01% 0m16.76s | 371064 ko | fiat-java/src/FiatP256Scalar.java | 0m15.92s | 334232 ko || +0m00.84s || 36832 ko | +5.27% | +11.01% 0m16.75s | 2144072 ko | ExtractionHaskell/bedrock2_unsaturated_solinas.hs | 0m16.53s | 2074184 ko || +0m00.21s || 69888 ko | +1.33% | +3.36% 0m16.73s | 406956 ko | fiat-json/src/curve25519_scalar_32.json | 0m16.02s | 450328 ko || +0m00.71s || -43372 ko | +4.43% | -9.63% 0m16.73s | 347524 ko | fiat-zig/src/secp256k1_montgomery_scalar_32.zig | 0m16.35s | 397760 ko || +0m00.37s || -50236 ko | +2.32% | -12.62% 0m16.72s | 390380 ko | fiat-zig/src/p256_scalar_32.zig | 0m16.18s | 356296 ko || +0m00.53s || 34084 ko | +3.33% | +9.56% 0m16.70s | 391092 ko | fiat-go/32/p256scalar/p256scalar.go | 0m16.94s | 366900 ko || -0m00.24s || 24192 ko | -1.41% | +6.59% 0m16.68s | 405796 ko | fiat-java/src/FiatCurve25519Scalar.java | 0m16.15s | 370228 ko || +0m00.53s || 35568 ko | +3.28% | +9.60% 0m16.66s | 378844 ko | fiat-rust/src/p256_scalar_32.rs | 0m15.98s | 411316 ko || +0m00.67s || -32472 ko | +4.25% | -7.89% 0m16.61s | 366928 ko | fiat-c/src/secp256k1_montgomery_scalar_32.c | 0m16.58s | 426780 ko || +0m00.03s || -59852 ko | +0.18% | -14.02% 0m16.59s | 340692 ko | fiat-rust/src/secp256k1_montgomery_32.rs | 0m16.47s | 353508 ko || +0m00.12s || -12816 ko | +0.72% | -3.62% 0m16.58s | 385436 ko | fiat-json/src/secp256k1_montgomery_32.json | 0m16.19s | 407896 ko || +0m00.38s || -22460 ko | +2.40% | -5.50% 0m16.55s | 416232 ko | fiat-go/32/curve25519scalar/curve25519scalar.go | 0m16.41s | 346260 ko || +0m00.14s || 69972 ko | +0.85% | +20.20% 0m16.53s | 338172 ko | fiat-java/src/FiatSecp256K1Montgomery.java | 0m16.15s | 423920 ko || +0m00.38s || -85748 ko | +2.35% | -20.22% 0m16.53s | 396224 ko | fiat-rust/src/secp256k1_montgomery_scalar_32.rs | 0m16.61s | 445068 ko || -0m00.07s || -48844 ko | -0.48% | -10.97% 0m16.50s | 2144128 ko | ExtractionHaskell/with_bedrock2_unsaturated_solinas.hs | 0m16.55s | 2072880 ko || -0m00.05s || 71248 ko | -0.30% | +3.43% 0m16.45s | 1139712 ko | Bedrock/End2End/Poly1305/Field1305.vo | 0m17.26s | 1137640 ko || -0m00.81s || 2072 ko | -4.69% | +0.18% 0m16.45s | 364804 ko | fiat-c/src/p256_scalar_32.c | 0m16.45s | 434352 ko || +0m00.00s || -69548 ko | +0.00% | -16.01% 0m16.36s | 436776 ko | fiat-zig/src/secp256k1_montgomery_32.zig | 0m16.01s | 437516 ko || +0m00.34s || -740 ko | +2.18% | -0.16% 0m16.33s | 359632 ko | fiat-zig/src/curve25519_scalar_32.zig | 0m15.80s | 434444 ko || +0m00.52s || -74812 ko | +3.35% | -17.22% 0m16.32s | 440340 ko | fiat-go/32/secp256k1montgomery/secp256k1montgomery.go | 0m16.19s | 415772 ko || +0m00.12s || 24568 ko | +0.80% | +5.90% 0m16.31s | 431364 ko | fiat-json/src/p256_scalar_32.json | 0m16.54s | 468452 ko || -0m00.23s || -37088 ko | -1.39% | -7.91% 0m16.28s | 418340 ko | fiat-c/src/secp256k1_montgomery_32.c | 0m16.07s | 354548 ko || +0m00.21s || 63792 ko | +1.30% | +17.99% 0m16.11s | 323148 ko | fiat-c/src/curve25519_scalar_32.c | 0m15.37s | 376208 ko || +0m00.74s || -53060 ko | +4.81% | -14.10% 0m16.09s | 429024 ko | fiat-rust/src/curve25519_scalar_32.rs | 0m16.31s | 405604 ko || -0m00.21s || 23420 ko | -1.34% | +5.77% 0m16.07s | 392824 ko | fiat-bedrock2/src/p256_32.c | 0m15.76s | 418500 ko || +0m00.31s || -25676 ko | +1.96% | -6.13% 0m15.73s | 2026232 ko | ExtractionHaskell/unsaturated_solinas.hs | 0m15.70s | 1972880 ko || +0m00.03s || 53352 ko | +0.19% | +2.70% 0m15.67s | 400632 ko | fiat-java/src/FiatP256.java | 0m15.23s | 347976 ko || +0m00.43s || 52656 ko | +2.88% | +15.13% 0m15.67s | 426864 ko | fiat-rust/src/p256_32.rs | 0m15.43s | 436980 ko || +0m00.24s || -10116 ko | +1.55% | -2.31% 0m15.65s | 433612 ko | fiat-go/32/p256/p256.go | 0m15.46s | 363800 ko || +0m00.18s || 69812 ko | +1.22% | +19.18% 0m15.65s | 332588 ko | fiat-zig/src/p256_32.zig | 0m15.39s | 407124 ko || +0m00.25s || -74536 ko | +1.68% | -18.30% 0m15.56s | 2010528 ko | ExtractionHaskell/with_bedrock2_dettman_multiplication.hs | 0m15.92s | 2039152 ko || -0m00.35s || -28624 ko | -2.26% | -1.40% 0m15.53s | 2010444 ko | ExtractionHaskell/bedrock2_dettman_multiplication.hs | 0m15.68s | 2040720 ko || -0m00.15s || -30276 ko | -0.95% | -1.48% 0m15.40s | 332344 ko | fiat-c/src/p256_32.c | 0m15.21s | 376848 ko || +0m00.18s || -44504 ko | +1.24% | -11.80% 0m15.29s | 1948284 ko | ExtractionHaskell/with_bedrock2_base_conversion.hs | 0m15.53s | 2016228 ko || -0m00.24s || -67944 ko | -1.54% | -3.36% 0m15.23s | 1959948 ko | ExtractionHaskell/with_bedrock2_saturated_solinas.hs | 0m15.52s | 2013692 ko || -0m00.28s || -53744 ko | -1.86% | -2.66% 0m15.22s | 1958896 ko | ExtractionHaskell/dettman_multiplication.hs | 0m15.10s | 1903264 ko || +0m00.12s || 55632 ko | +0.79% | +2.92% 0m15.15s | 1948672 ko | ExtractionHaskell/bedrock2_base_conversion.hs | 0m15.63s | 2015624 ko || -0m00.48s || -66952 ko | -3.07% | -3.32% 0m15.12s | 445592 ko | fiat-json/src/p256_32.json | 0m15.46s | 416848 ko || -0m00.34s || 28744 ko | -2.19% | +6.89% 0m15.11s | 1960852 ko | ExtractionHaskell/bedrock2_saturated_solinas.hs | 0m15.44s | 2013416 ko || -0m00.33s || -52564 ko | -2.13% | -2.61% 0m14.88s | 1955220 ko | ExtractionHaskell/base_conversion.hs | 0m14.93s | 1897380 ko || -0m00.04s || 57840 ko | -0.33% | +3.04% 0m14.86s | 1921176 ko | ExtractionHaskell/saturated_solinas.hs | 0m14.96s | 1916928 ko || -0m00.10s || 4248 ko | -0.66% | +0.22% 0m11.31s | 199152 ko | fiat-bedrock2/src/p384_scalar_64.c | 0m11.18s | 194984 ko || +0m00.13s || 4168 ko | +1.16% | +2.13% 0m11.21s | 199888 ko | fiat-go/64/p384scalar/p384scalar.go | 0m11.15s | 164128 ko || +0m00.06s || 35760 ko | +0.53% | +21.78% 0m11.17s | 1708132 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo | 0m11.30s | 1703996 ko || -0m00.13s || 4136 ko | -1.15% | +0.24% 0m10.92s | 1035420 ko | BoundsPipeline.vo | 0m11.20s | 1036784 ko || -0m00.27s || -1364 ko | -2.49% | -0.13% 0m10.91s | 169592 ko | fiat-json/src/p384_scalar_64.json | 0m10.81s | 184092 ko || +0m00.09s || -14500 ko | +0.92% | -7.87% 0m10.87s | 176344 ko | fiat-zig/src/p384_scalar_64.zig | 0m10.57s | 192372 ko || +0m00.29s || -16028 ko | +2.83% | -8.33% 0m10.73s | 166616 ko | fiat-rust/src/p384_scalar_64.rs | 0m10.84s | 176032 ko || -0m00.10s || -9416 ko | -1.01% | -5.34% 0m10.58s | 154460 ko | fiat-c/src/p384_scalar_64.c | 0m10.71s | 142320 ko || -0m00.13s || 12140 ko | -1.21% | +8.53% 0m10.15s | 1304732 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo | 0m10.24s | 1304688 ko || -0m00.08s || 44 ko | -0.87% | +0.00% 0m09.59s | 195012 ko | fiat-bedrock2/src/p384_64.c | 0m09.53s | 205984 ko || +0m00.06s || -10972 ko | +0.62% | -5.32% 0m09.54s | 255304 ko | fiat-bedrock2/src/p224_32.c | 0m09.46s | 246228 ko || +0m00.07s || 9076 ko | +0.84% | +3.68% 0m09.38s | 235988 ko | fiat-json/src/p224_32.json | 0m09.14s | 243676 ko || +0m00.24s || -7688 ko | +2.62% | -3.15% 0m09.29s | 195668 ko | fiat-json/src/p384_64.json | 0m09.24s | 173592 ko || +0m00.04s || 22076 ko | +0.54% | +12.71% 0m09.26s | 245908 ko | fiat-java/src/FiatP224.java | 0m09.02s | 210104 ko || +0m00.24s || 35804 ko | +2.66% | +17.04% 0m09.25s | 170924 ko | fiat-go/64/p384/p384.go | 0m09.35s | 160844 ko || -0m00.09s || 10080 ko | -1.06% | +6.26% 0m09.20s | 1040012 ko | PushButtonSynthesis/BaseConversion.vo | 0m09.41s | 1037912 ko || -0m00.21s || 2100 ko | -2.23% | +0.20% 0m09.14s | 225000 ko | fiat-go/32/p224/p224.go | 0m09.39s | 230444 ko || -0m00.25s || -5444 ko | -2.66% | -2.36% 0m09.11s | 253348 ko | fiat-rust/src/p224_32.rs | 0m09.20s | 245628 ko || -0m00.08s || 7720 ko | -0.97% | +3.14% 0m09.11s | 166552 ko | fiat-zig/src/p384_64.zig | 0m09.31s | 141172 ko || -0m00.20s || 25380 ko | -2.14% | +17.97% 0m09.10s | 167020 ko | fiat-c/src/p384_64.c | 0m09.28s | 146704 ko || -0m00.17s || 20316 ko | -1.93% | +13.84% 0m09.09s | 254100 ko | fiat-zig/src/p224_32.zig | 0m08.87s | 222884 ko || +0m00.22s || 31216 ko | +2.48% | +14.00% 0m08.96s | 232884 ko | fiat-c/src/p224_32.c | 0m08.97s | 240356 ko || -0m00.00s || -7472 ko | -0.11% | -3.10% 0m08.73s | 147896 ko | fiat-rust/src/p384_64.rs | 0m09.22s | 165796 ko || -0m00.49s || -17900 ko | -5.31% | -10.79% 0m08.26s | 1009244 ko | PushButtonSynthesis/SmallExamples.vo | 0m08.45s | 1008344 ko || -0m00.18s || 900 ko | -2.24% | +0.08% 0m08.26s | 119472 ko | fiat-json/src/p448_solinas_32.json | 0m08.29s | 123884 ko || -0m00.02s || -4412 ko | -0.36% | -3.56% 0m08.16s | 1050960 ko | PushButtonSynthesis/Primitives.vo | 0m08.27s | 1050876 ko || -0m00.10s || 84 ko | -1.33% | +0.00% 0m07.93s | 591100 ko | Rewriter/Passes/RelaxBitwidthAdcSbb.vo | 0m08.19s | 591176 ko || -0m00.25s || -76 ko | -3.17% | -0.01% 0m07.91s | 61592 ko | fiat-zig/src/p448_solinas_32.zig | 0m07.94s | 61704 ko || -0m00.03s || -112 ko | -0.37% | -0.18% 0m07.89s | 59392 ko | fiat-c/src/p448_solinas_32.c | 0m07.94s | 56764 ko || -0m00.05s || 2628 ko | -0.62% | +4.62% 0m07.88s | 61076 ko | fiat-rust/src/p448_solinas_32.rs | 0m08.00s | 57600 ko || -0m00.12s || 3476 ko | -1.50% | +6.03% 0m07.12s | 1043600 ko | PushButtonSynthesis/SolinasReduction.vo | 0m07.38s | 1043572 ko || -0m00.25s || 28 ko | -3.52% | +0.00% 0m06.64s | 52476 ko | fiat-go/64/p521/p521.go | 0m06.25s | 49644 ko || +0m00.38s || 2832 ko | +6.23% | +5.70% 0m06.27s | 574792 ko | Rewriter/Passes/NoSelect.vo | 0m06.41s | 577812 ko || -0m00.14s || -3020 ko | -2.18% | -0.52% 0m06.26s | 1048224 ko | PushButtonSynthesis/BarrettReduction.vo | 0m06.20s | 1051084 ko || +0m00.05s || -2860 ko | +0.96% | -0.27% 0m06.22s | 1132216 ko | CLI.vo | 0m06.30s | 1130060 ko || -0m00.08s || 2156 ko | -1.26% | +0.19% 0m05.96s | 1144288 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo | 0m06.15s | 1142040 ko || -0m00.19s || 2248 ko | -3.08% | +0.19% 0m05.54s | 68872 ko | fiat-bedrock2/src/p521_64.c | 0m05.56s | 68208 ko || -0m00.01s || 664 ko | -0.35% | +0.97% 0m05.42s | 51340 ko | fiat-json/src/p521_64.json | 0m05.43s | 51520 ko || -0m00.00s || -180 ko | -0.18% | -0.34% 0m05.30s | 37436 ko | fiat-zig/src/p521_64.zig | 0m04.77s | 37212 ko || +0m00.53s || 224 ko | +11.11% | +0.60% 0m04.82s | 37880 ko | fiat-rust/src/p521_64.rs | 0m05.45s | 38100 ko || -0m00.62s || -220 ko | -11.55% | -0.57% 0m04.76s | 37380 ko | fiat-c/src/p521_64.c | 0m05.37s | 37352 ko || -0m00.61s || 28 ko | -11.35% | +0.07% 0m04.66s | 1038068 ko | PushButtonSynthesis/DettmanMultiplication.vo | 0m04.63s | 1038160 ko || +0m00.03s || -92 ko | +0.64% | -0.00% 0m04.51s | 1074152 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m04.59s | 1074372 ko || -0m00.08s || -220 ko | -1.74% | -0.02% 0m04.24s | 1047736 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m04.41s | 1047768 ko || -0m00.16s || -32 ko | -3.85% | -0.00% 0m04.01s | 1501044 ko | Bedrock/Everything.vo | 0m04.01s | 1501100 ko || +0m00.00s || -56 ko | +0.00% | -0.00% 0m03.81s | 1051824 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m03.77s | 1050712 ko || +0m00.04s || 1112 ko | +1.06% | +0.10% 0m03.50s | 1367412 ko | Everything.vo | 0m03.59s | 1367556 ko || -0m00.08s || -144 ko | -2.50% | -0.01% 0m03.06s | 537952 ko | Rewriter/Passes/ArithWithRelaxedCasts.vo | 0m03.15s | 539144 ko || -0m00.08s || -1192 ko | -2.85% | -0.22% 0m02.98s | 1013864 ko | Bedrock/Field/Translation/Cmd.vo | 0m02.98s | 1014664 ko || +0m00.00s || -800 ko | +0.00% | -0.07% 0m02.96s | 1083180 ko | Rewriter/PerfTesting/Core.vo | 0m03.04s | 1083012 ko || -0m00.08s || 168 ko | -2.63% | +0.01% 0m02.94s | 70004 ko | fiat-go/64/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go | 0m02.80s | 69640 ko || +0m00.14s || 364 ko | +5.00% | +0.52% 0m02.93s | 69652 ko | fiat-go/64/p256scalar/p256scalar.go | 0m02.77s | 69300 ko || +0m00.16s || 352 ko | +5.77% | +0.50% 0m02.92s | 539268 ko | Rewriter/Passes/AddAssocLeft.vo | 0m02.99s | 537676 ko || -0m00.07s || 1592 ko | -2.34% | +0.29% 0m02.90s | 1126644 ko | StandaloneHaskellMain.vo | 0m02.85s | 1124644 ko || +0m00.04s || 2000 ko | +1.75% | +0.17% 0m02.86s | 1355272 ko | PerfTesting/PerfTestPrint.vo | 0m02.97s | 1353376 ko || -0m00.11s || 1896 ko | -3.70% | +0.14% 0m02.83s | 74888 ko | fiat-json/src/p256_scalar_64.json | 0m02.73s | 69468 ko || +0m00.10s || 5420 ko | +3.66% | +7.80% 0m02.79s | 84092 ko | fiat-bedrock2/src/p256_scalar_64.c | 0m02.79s | 86516 ko || +0m00.00s || -2424 ko | +0.00% | -2.80% 0m02.76s | 87368 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_64.c | 0m02.77s | 86936 ko || -0m00.01s || 432 ko | -0.36% | +0.49% 0m02.76s | 57416 ko | fiat-go/64/p448solinas/p448solinas.go | 0m02.58s | 51820 ko || +0m00.17s || 5596 ko | +6.97% | +10.79% 0m02.76s | 73888 ko | fiat-json/src/secp256k1_montgomery_scalar_64.json | 0m02.73s | 75908 ko || +0m00.02s || -2020 ko | +1.09% | -2.66% 0m02.74s | 1077636 ko | Bedrock/Field/Stringification/Stringification.vo | 0m02.78s | 1076572 ko || -0m00.03s || 1064 ko | -1.43% | +0.09% 0m02.73s | 1010148 ko | Bedrock/Field/Translation/Func.vo | 0m02.82s | 1008988 ko || -0m00.08s || 1160 ko | -3.19% | +0.11% 0m02.72s | 64580 ko | fiat-zig/src/p256_scalar_64.zig | 0m02.71s | 62528 ko || +0m00.01s || 2052 ko | +0.36% | +3.28% 0m02.69s | 63552 ko | fiat-go/64/secp256k1montgomery/secp256k1montgomery.go | 0m02.51s | 67572 ko || +0m00.18s || -4020 ko | +7.17% | -5.94% 0m02.69s | 61992 ko | fiat-rust/src/p256_scalar_64.rs | 0m02.75s | 66124 ko || -0m00.06s || -4132 ko | -2.18% | -6.24% 0m02.69s | 63084 ko | fiat-rust/src/secp256k1_montgomery_scalar_64.rs | 0m02.71s | 66576 ko || -0m00.02s || -3492 ko | -0.73% | -5.24% 0m02.68s | 59288 ko | fiat-c/src/p256_scalar_64.c | 0m02.70s | 62336 ko || -0m00.02s || -3048 ko | -0.74% | -4.88% 0m02.67s | 1068128 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo | 0m02.80s | 1068044 ko || -0m00.12s || 84 ko | -4.64% | +0.00% 0m02.67s | 68464 ko | fiat-c/src/secp256k1_montgomery_scalar_64.c | 0m02.70s | 61160 ko || -0m00.03s || 7304 ko | -1.11% | +11.94% 0m02.66s | 1153388 ko | Bedrock/Standalone/StandaloneHaskellMain.vo | 0m02.71s | 1151268 ko || -0m00.04s || 2120 ko | -1.84% | +0.18% 0m02.66s | 64136 ko | fiat-zig/src/secp256k1_montgomery_scalar_64.zig | 0m02.65s | 62200 ko || +0m00.01s || 1936 ko | +0.37% | +3.11% 0m02.65s | 1103644 ko | StandaloneOCamlMain.vo | 0m02.61s | 1103620 ko || +0m00.04s || 24 ko | +1.53% | +0.00% 0m02.64s | 1151352 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m02.71s | 1151372 ko || -0m00.06s || -20 ko | -2.58% | -0.00% 0m02.57s | 535856 ko | Rewriter/Passes/FlattenThunkedRects.vo | 0m02.66s | 535192 ko || -0m00.09s || 664 ko | -3.38% | +0.12% 0m02.52s | 84488 ko | fiat-bedrock2/src/secp256k1_montgomery_64.c | 0m02.47s | 93372 ko || +0m00.04s || -8884 ko | +2.02% | -9.51% 0m02.52s | 68592 ko | fiat-json/src/secp256k1_montgomery_64.json | 0m02.46s | 75364 ko || +0m00.06s || -6772 ko | +2.43% | -8.98% 0m02.49s | 1073080 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo | 0m02.66s | 1071116 ko || -0m00.16s || 1964 ko | -6.39% | +0.18% 0m02.48s | 1137168 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m02.76s | 1135252 ko || -0m00.27s || 1916 ko | -10.14% | +0.16% 0m02.46s | 63516 ko | fiat-go/64/curve25519scalar/curve25519scalar.go | 0m02.31s | 70228 ko || +0m00.14s || -6712 ko | +6.49% | -9.55% 0m02.42s | 1051400 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo | 0m02.46s | 1051612 ko || -0m00.04s || -212 ko | -1.62% | -0.02% 0m02.42s | 60544 ko | fiat-rust/src/secp256k1_montgomery_64.rs | 0m02.42s | 60264 ko || +0m00.00s || 280 ko | +0.00% | +0.46% 0m02.42s | 65732 ko | fiat-zig/src/secp256k1_montgomery_64.zig | 0m02.40s | 57992 ko || +0m00.02s || 7740 ko | +0.83% | +13.34% 0m02.41s | 60148 ko | fiat-c/src/secp256k1_montgomery_64.c | 0m02.44s | 60532 ko || -0m00.02s || -384 ko | -1.22% | -0.63% 0m02.37s | 1051572 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo | 0m02.46s | 1051524 ko || -0m00.08s || 48 ko | -3.65% | +0.00% 0m02.35s | 1050808 ko | Bedrock/Field/Translation/Parameters/FE310.vo | 0m02.42s | 1051668 ko || -0m00.06s || -860 ko | -2.89% | -0.08% 0m02.35s | 78788 ko | fiat-bedrock2/src/curve25519_scalar_64.c | 0m02.35s | 77892 ko || +0m00.00s || 896 ko | +0.00% | +1.15% 0m02.34s | 1047512 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m02.33s | 1047596 ko || +0m00.00s || -84 ko | +0.42% | -0.00% 0m02.31s | 69108 ko | fiat-json/src/curve25519_scalar_64.json | 0m02.30s | 69200 ko || +0m00.01s || -92 ko | +0.43% | -0.13% 0m02.28s | 60412 ko | fiat-rust/src/curve25519_scalar_64.rs | 0m02.31s | 64076 ko || -0m00.03s || -3664 ko | -1.29% | -5.71% 0m02.25s | 67320 ko | fiat-c/src/curve25519_scalar_64.c | 0m02.29s | 59928 ko || -0m00.04s || 7392 ko | -1.74% | +12.33% 0m02.25s | 57700 ko | fiat-zig/src/curve25519_scalar_64.zig | 0m02.25s | 63136 ko || +0m00.00s || -5436 ko | +0.00% | -8.60% 0m02.17s | 541552 ko | Rewriter/Passes/UnfoldValueBarrier.vo | 0m02.27s | 541600 ko || -0m00.10s || -48 ko | -4.40% | -0.00% 0m02.10s | 540980 ko | Rewriter/Passes/StripLiteralCasts.vo | 0m02.20s | 539800 ko || -0m00.10s || 1180 ko | -4.54% | +0.21% 0m02.10s | 63292 ko | fiat-go/64/p224/p224.go | 0m01.86s | 61856 ko || +0m00.24s || 1436 ko | +12.90% | +2.32% 0m02.08s | 38528 ko | fiat-go/32/curve25519/curve25519.go | 0m02.07s | 36104 ko || +0m00.01s || 2424 ko | +0.48% | +6.71% 0m02.07s | 68844 ko | fiat-bedrock2/src/p448_solinas_64.c | 0m02.13s | 66964 ko || -0m00.06s || 1880 ko | -2.81% | +2.80% 0m02.05s | 63476 ko | fiat-go/64/p256/p256.go | 0m01.84s | 62612 ko || +0m00.20s || 864 ko | +11.41% | +1.37% 0m02.02s | 69516 ko | fiat-bedrock2/src/curve25519_32.c | 0m01.99s | 64620 ko || +0m00.03s || 4896 ko | +1.50% | +7.57% 0m01.97s | 536652 ko | Rewriter/Passes/ToFancy.vo | 0m02.01s | 537484 ko || -0m00.03s || -832 ko | -1.99% | -0.15% 0m01.96s | 52072 ko | fiat-json/src/p448_solinas_64.json | 0m01.92s | 49556 ko || +0m00.04s || 2516 ko | +2.08% | +5.07% 0m01.91s | 78628 ko | fiat-bedrock2/src/p224_64.c | 0m01.91s | 79832 ko || +0m00.00s || -1204 ko | +0.00% | -1.50% 0m01.90s | 35620 ko | fiat-c/src/p448_solinas_64.c | 0m01.93s | 35532 ko || -0m00.03s || 88 ko | -1.55% | +0.24% 0m01.90s | 35992 ko | fiat-rust/src/p448_solinas_64.rs | 0m01.93s | 37888 ko || -0m00.03s || -1896 ko | -1.55% | -5.00% 0m01.90s | 36340 ko | fiat-zig/src/p448_solinas_64.zig | 0m01.90s | 38132 ko || +0m00.00s || -1792 ko | +0.00% | -4.69% 0m01.89s | 68480 ko | fiat-json/src/p224_64.json | 0m01.93s | 76344 ko || -0m00.04s || -7864 ko | -2.07% | -10.30% 0m01.85s | 79464 ko | fiat-bedrock2/src/p256_64.c | 0m01.85s | 80384 ko || +0m00.00s || -920 ko | +0.00% | -1.14% 0m01.84s | 69732 ko | fiat-json/src/p256_64.json | 0m01.85s | 68332 ko || -0m00.01s || 1400 ko | -0.54% | +2.04% 0m01.84s | 60888 ko | fiat-zig/src/p224_64.zig | 0m01.87s | 60200 ko || -0m00.03s || 688 ko | -1.60% | +1.14% 0m01.83s | 51832 ko | fiat-json/src/curve25519_32.json | 0m01.91s | 54384 ko || -0m00.07s || -2552 ko | -4.18% | -4.69% 0m01.82s | 57456 ko | fiat-zig/src/p256_64.zig | 0m01.79s | 57520 ko || +0m00.03s || -64 ko | +1.67% | -0.11% 0m01.81s | 60544 ko | fiat-rust/src/p224_64.rs | 0m01.87s | 61580 ko || -0m00.06s || -1036 ko | -3.20% | -1.68% 0m01.77s | 58112 ko | fiat-c/src/p224_64.c | 0m01.78s | 61864 ko || -0m00.01s || -3752 ko | -0.56% | -6.06% 0m01.77s | 60016 ko | fiat-rust/src/p256_64.rs | 0m01.78s | 60884 ko || -0m00.01s || -868 ko | -0.56% | -1.42% 0m01.76s | 36740 ko | fiat-java/src/FiatCurve25519.java | 0m01.70s | 35152 ko || +0m00.06s || 1588 ko | +3.52% | +4.51% 0m01.76s | 35116 ko | fiat-rust/src/curve25519_32.rs | 0m01.76s | 34160 ko || +0m00.00s || 956 ko | +0.00% | +2.79% 0m01.75s | 35380 ko | fiat-zig/src/curve25519_32.zig | 0m01.75s | 35084 ko || +0m00.00s || 296 ko | +0.00% | +0.84% 0m01.74s | 35840 ko | fiat-c/src/curve25519_32.c | 0m01.76s | 34260 ko || -0m00.02s || 1580 ko | -1.13% | +4.61% 0m01.74s | 65196 ko | fiat-c/src/p256_64.c | 0m01.76s | 62724 ko || -0m00.02s || 2472 ko | -1.13% | +3.94% 0m01.45s | 596340 ko | CompilersTestCases.vo | 0m01.51s | 596224 ko || -0m00.06s || 116 ko | -3.97% | +0.01% 0m01.44s | 53596 ko | fiat-bedrock2/src/secp256k1_dettman_32.c | 0m01.45s | 51196 ko || -0m00.01s || 2400 ko | -0.68% | +4.68% 0m01.28s | 42572 ko | fiat-json/src/secp256k1_dettman_32.json | 0m01.30s | 43796 ko || -0m00.02s || -1224 ko | -1.53% | -2.79% 0m01.22s | 25936 ko | fiat-c/src/secp256k1_dettman_32.c | 0m01.23s | 26436 ko || -0m00.01s || -500 ko | -0.81% | -1.89% 0m01.22s | 26988 ko | fiat-go/32/secp256k1dettman/secp256k1dettman.go | 0m01.26s | 26796 ko || -0m00.04s || 192 ko | -3.17% | +0.71% 0m01.22s | 27128 ko | fiat-java/src/FiatSecp256K1Dettman.java | 0m01.21s | 27648 ko || +0m00.01s || -520 ko | +0.82% | -1.88% 0m01.22s | 26456 ko | fiat-rust/src/secp256k1_dettman_32.rs | 0m01.24s | 26404 ko || -0m00.02s || 52 ko | -1.61% | +0.19% 0m01.20s | 26264 ko | fiat-zig/src/secp256k1_dettman_32.zig | 0m01.21s | 26620 ko || -0m00.01s || -356 ko | -0.82% | -1.33% 0m00.72s | 33336 ko | fiat-go/64/curve25519/curve25519.go | 0m00.62s | 33132 ko || +0m00.09s || 204 ko | +16.12% | +0.61% 0m00.63s | 438660 ko | Rewriter/Rules.vo | 0m00.63s | 436796 ko || +0m00.00s || 1864 ko | +0.00% | +0.42% 0m00.58s | 552492 ko | Rewriter/All.vo | 0m00.60s | 552492 ko || -0m00.02s || 0 ko | -3.33% | +0.00% 0m00.54s | 123656 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi | 0m00.54s | 122456 ko || +0m00.00s || 1200 ko | +0.00% | +0.97% 0m00.54s | 123868 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi | 0m00.55s | 122976 ko || -0m00.01s || 892 ko | -1.81% | +0.72% 0m00.54s | 120496 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi | 0m00.56s | 122432 ko || -0m00.02s || -1936 ko | -3.57% | -1.58% 0m00.53s | 120220 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi | 0m00.54s | 120352 ko || -0m00.01s || -132 ko | -1.85% | -0.10% 0m00.53s | 122856 ko | ExtractionOCaml/unsaturated_solinas.cmi | 0m00.52s | 121012 ko || +0m00.01s || 1844 ko | +1.92% | +1.52% 0m00.53s | 122964 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi | 0m00.56s | 123648 ko || -0m00.03s || -684 ko | -5.35% | -0.55% 0m00.53s | 39636 ko | fiat-bedrock2/src/curve25519_64.c | 0m00.50s | 38928 ko || +0m00.03s || 708 ko | +6.00% | +1.81% 0m00.52s | 123624 ko | ExtractionOCaml/bedrock2_base_conversion.cmi | 0m00.53s | 123936 ko || -0m00.01s || -312 ko | -1.88% | -0.25% 0m00.52s | 120356 ko | ExtractionOCaml/dettman_multiplication.cmi | 0m00.50s | 120344 ko || +0m00.02s || 12 ko | +4.00% | +0.00% 0m00.52s | 123888 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi | 0m00.52s | 123416 ko || +0m00.00s || 472 ko | +0.00% | +0.38% 0m00.52s | 121844 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.cmi | 0m00.52s | 121848 ko || +0m00.00s || -4 ko | +0.00% | -0.00% 0m00.51s | 122700 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi | 0m00.53s | 123096 ko || -0m00.02s || -396 ko | -3.77% | -0.32% 0m00.50s | 120684 ko | ExtractionOCaml/base_conversion.cmi | 0m00.50s | 122432 ko || +0m00.00s || -1748 ko | +0.00% | -1.42% 0m00.50s | 120748 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi | 0m00.57s | 120620 ko || -0m00.06s || 128 ko | -12.28% | +0.10% 0m00.50s | 120344 ko | ExtractionOCaml/saturated_solinas.cmi | 0m00.51s | 120300 ko || -0m00.01s || 44 ko | -1.96% | +0.03% 0m00.50s | 28344 ko | fiat-zig/src/curve25519_64.zig | 0m00.46s | 28560 ko || +0m00.03s || -216 ko | +8.69% | -0.75% 0m00.49s | 123236 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi | 0m00.53s | 122576 ko || -0m00.04s || 660 ko | -7.54% | +0.53% 0m00.49s | 120500 ko | ExtractionOCaml/word_by_word_montgomery.cmi | 0m00.48s | 120356 ko || +0m00.01s || 144 ko | +2.08% | +0.11% 0m00.49s | 35980 ko | fiat-json/src/curve25519_64.json | 0m00.52s | 34660 ko || -0m00.03s || 1320 ko | -5.76% | +3.80% 0m00.49s | 28488 ko | fiat-rust/src/curve25519_64.rs | 0m00.47s | 27384 ko || +0m00.02s || 1104 ko | +4.25% | +4.03% 0m00.48s | 121720 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi | 0m00.52s | 122768 ko || -0m00.04s || -1048 ko | -7.69% | -0.85% 0m00.47s | 119616 ko | ExtractionOCaml/solinas_reduction.cmi | 0m00.49s | 120324 ko || -0m00.02s || -708 ko | -4.08% | -0.58% 0m00.47s | 28124 ko | fiat-c/src/curve25519_64.c | 0m00.45s | 28304 ko || +0m00.01s || -180 ko | +4.44% | -0.63% 0m00.44s | 37236 ko | fiat-go/64/curve25519solinas/curve25519solinas.go | 0m00.40s | 37736 ko || +0m00.03s || -500 ko | +9.99% | -1.32% 0m00.43s | 38744 ko | fiat-json/src/curve25519_solinas_64.json | 0m00.43s | 40512 ko || +0m00.00s || -1768 ko | +0.00% | -4.36% 0m00.43s | 38224 ko | fiat-rust/src/curve25519_solinas_64.rs | 0m00.41s | 37192 ko || +0m00.02s || 1032 ko | +4.87% | +2.77% 0m00.42s | 45732 ko | fiat-bedrock2/src/curve25519_solinas_64.c | 0m00.40s | 42468 ko || +0m00.01s || 3264 ko | +4.99% | +7.68% 0m00.42s | 37052 ko | fiat-zig/src/curve25519_solinas_64.zig | 0m00.41s | 36628 ko || +0m00.01s || 424 ko | +2.43% | +1.15% 0m00.38s | 37156 ko | fiat-c/src/curve25519_solinas_64.c | 0m00.42s | 37160 ko || -0m00.03s || -4 ko | -9.52% | -0.01% 0m00.29s | 26484 ko | fiat-go/32/poly1305/poly1305.go | 0m00.28s | 26668 ko || +0m00.00s || -184 ko | +3.57% | -0.68% 0m00.26s | 33824 ko | fiat-bedrock2/src/poly1305_32.c | 0m00.26s | 33836 ko || +0m00.00s || -12 ko | +0.00% | -0.03% 0m00.24s | 26896 ko | fiat-go/64/secp256k1dettman/secp256k1dettman.go | 0m00.22s | 26224 ko || +0m00.01s || 672 ko | +9.09% | +2.56% 0m00.24s | 26316 ko | fiat-java/src/FiatPoly1305.java | 0m00.22s | 25696 ko || +0m00.01s || 620 ko | +9.09% | +2.41% 0m00.24s | 31548 ko | fiat-json/src/poly1305_32.json | 0m00.24s | 31200 ko || +0m00.00s || 348 ko | +0.00% | +1.11% 0m00.23s | 26104 ko | fiat-c/src/poly1305_32.c | 0m00.21s | 25912 ko || +0m00.02s || 192 ko | +9.52% | +0.74% 0m00.23s | 27116 ko | fiat-go/64/poly1305/poly1305.go | 0m00.17s | 27576 ko || +0m00.06s || -460 ko | +35.29% | -1.66% 0m00.23s | 26228 ko | fiat-rust/src/poly1305_32.rs | 0m00.22s | 26228 ko || +0m00.01s || 0 ko | +4.54% | +0.00% 0m00.22s | 31180 ko | fiat-bedrock2/src/secp256k1_dettman_64.c | 0m00.23s | 30968 ko || -0m00.01s || 212 ko | -4.34% | +0.68% 0m00.21s | 25520 ko | fiat-zig/src/poly1305_32.zig | 0m00.21s | 25420 ko || +0m00.00s || 100 ko | +0.00% | +0.39% 0m00.20s | 25196 ko | fiat-json/src/secp256k1_dettman_64.json | 0m00.19s | 24872 ko || +0m00.01s || 324 ko | +5.26% | +1.30% 0m00.20s | 22184 ko | fiat-zig/src/secp256k1_dettman_64.zig | 0m00.18s | 21864 ko || +0m00.02s || 320 ko | +11.11% | +1.46% 0m00.18s | 21800 ko | fiat-c/src/secp256k1_dettman_64.c | 0m00.18s | 21800 ko || +0m00.00s || 0 ko | +0.00% | +0.00% 0m00.18s | 22084 ko | fiat-rust/src/secp256k1_dettman_64.rs | 0m00.18s | 22376 ko || +0m00.00s || -292 ko | +0.00% | -1.30% 0m00.17s | 61932 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi | 0m00.19s | 62248 ko || -0m00.01s || -316 ko | -10.52% | -0.50% 0m00.16s | 62528 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi | 0m00.16s | 61452 ko || +0m00.00s || 1076 ko | +0.00% | +1.75% 0m00.15s | 28964 ko | fiat-json/src/poly1305_64.json | 0m00.14s | 27736 ko || +0m00.00s || 1228 ko | +7.14% | +4.42% 0m00.13s | 25196 ko | fiat-rust/src/poly1305_64.rs | 0m00.12s | 24336 ko || +0m00.01s || 860 ko | +8.33% | +3.53% 0m00.12s | 29576 ko | fiat-bedrock2/src/poly1305_64.c | 0m00.12s | 29648 ko || +0m00.00s || -72 ko | +0.00% | -0.24% 0m00.12s | 24992 ko | fiat-c/src/poly1305_64.c | 0m00.12s | 24612 ko || +0m00.00s || 380 ko | +0.00% | +1.54% 0m00.12s | 24928 ko | fiat-zig/src/poly1305_64.zig | 0m00.13s | 24612 ko || -0m00.01s || 316 ko | -7.69% | +1.28% ``` </p> </details>

JasonGross added the awaiting-timing-info label Dec 8, 2023

JasonGross commented Dec 8, 2023

View reviewed changes

JasonGross force-pushed the more-rewrite-simple branch 2 times, most recently from b3d80ad to 0f33a20 Compare December 8, 2023 05:13

JasonGross added needs: fixing and removed awaiting-timing-info labels Dec 8, 2023

JasonGross added a commit to JasonGross/fiat-crypto that referenced this pull request Dec 10, 2023

Augment rewrite rule proving tactics for saturated arithmetic

5eb3704

For mit-plv#1609 and mit-plv#1777

JasonGross mentioned this pull request Dec 10, 2023

Augment rewrite rule proving tactics for saturated arithmetic #1783

Merged

JasonGross force-pushed the more-rewrite-simple branch from 0f33a20 to 193747f Compare December 10, 2023 00:46

JasonGross added a commit to JasonGross/fiat-crypto that referenced this pull request Dec 10, 2023

Augment rewrite rule proving tactics for saturated arithmetic

0055c8c

For mit-plv#1609 and mit-plv#1777

JasonGross force-pushed the more-rewrite-simple branch from 193747f to f7226e7 Compare December 10, 2023 03:44

JasonGross added a commit that referenced this pull request Dec 10, 2023

Augment rewrite rule proving tactics for saturated arithmetic (#1783)

a407ad0

For #1609 and #1777

JasonGross force-pushed the more-rewrite-simple branch from f7226e7 to e3a6602 Compare December 10, 2023 10:03

JasonGross assigned andres-erbsen Dec 23, 2023

JasonGross marked this pull request as draft December 23, 2023 16:57

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Unobjectionable rewrite rules for saturated arithmetic #1777

Unobjectionable rewrite rules for saturated arithmetic #1777

JasonGross commented Dec 8, 2023

JasonGross Dec 8, 2023

JasonGross Dec 8, 2023

JasonGross Dec 8, 2023

JasonGross commented Dec 8, 2023

Unobjectionable rewrite rules for saturated arithmetic #1777

Are you sure you want to change the base?

Unobjectionable rewrite rules for saturated arithmetic #1777

Conversation

JasonGross commented Dec 8, 2023

JasonGross Dec 8, 2023

Choose a reason for hiding this comment

JasonGross Dec 8, 2023

Choose a reason for hiding this comment

JasonGross Dec 8, 2023

Choose a reason for hiding this comment

JasonGross commented Dec 8, 2023